{
 "cells": [
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {},
   "outputs": [],
   "source": [
    "# -*- coding: utf-8 -*-\n",
    "from miasm.analysis.machine import Machine\n",
    "from miasm.arch.x86.arch import mn_x86\n",
    "from miasm.ir.symbexec import SymbolicExecutionEngine\n",
    "from miasm.expression.expression import ExprInt, ExprMem, ExprId, LocKey\n",
    "from miasm.arch.x86.regs import *\n",
    "from miasm.analysis.binary import Container\n",
    "from miasm.core.locationdb import LocationDB\n",
    "from future.utils import viewitems\n",
    "from argparse import ArgumentParser\n",
    "import sys, z3"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {},
   "outputs": [],
   "source": [
    "!unzip -n -P infected x-tunnel.zip\n",
    "!unzip -n -P infected anel.zip"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {},
   "outputs": [],
   "source": [
    "filename = 'x-tunnel.bin'\n",
    "target_addr = 0x405710\n",
    "#filename = '../hands-on1/test-add-bcf.bin'\n",
    "#target_addr = 0x80483F0\n",
    "#filename = '../hands-on1/test-hello-bcf.bin'\n",
    "#target_addr = 0x80483F0\n",
    "#filename = '../hands-on1/test-mod2-bcf.bin'\n",
    "#target_addr = 0x80483F0\n",
    "#filename = '../hands-on1/test-add-opaque.bin'\n",
    "#target_addr = 0x8048471\n",
    "idc = True"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {},
   "outputs": [],
   "source": [
    "%run solved/simple_explore_smt.ipynb # from simple_explore_smt import *"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {},
   "outputs": [],
   "source": [
    "def to_idc(lockeys, asmcfg):\n",
    "\n",
    "    header = '''\n",
    "#include <idc.idc>\n",
    "static main(){\n",
    "'''\n",
    "    footer = '''\n",
    "}\n",
    "'''\n",
    "    body = ''\n",
    "    f = open('op-color.idc', 'w')\n",
    "    for lbl in lockeys:\n",
    "        asmblk = asmcfg.loc_key_to_block(lbl)\n",
    "        if asmblk:\n",
    "            for l in asmblk.lines:\n",
    "                body += 'SetColor(0x%08x, CIC_ITEM, 0xc7c7ff);\\n'%(l.offset)\n",
    "    \n",
    "    f.write(header+body+footer)\n",
    "    f.close()"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {},
   "outputs": [],
   "source": [
    "loc_db = LocationDB()\n",
    "with open(filename, 'rb') as fstream:                                      \n",
    "    cont = Container.from_stream(fstream, loc_db)\n",
    "\n",
    "machine = Machine('x86_32')\n",
    "mdis = machine.dis_engine(cont.bin_stream, follow_call=False, loc_db=cont.loc_db)\n",
    "ir_arch = machine.ira(mdis.loc_db)\n",
    "\n",
    "# Disassemble the targeted function\n",
    "asmcfg = mdis.dis_multiblock(target_addr)\n",
    "\n",
    "# IRCFG\n",
    "ircfg = ir_arch.new_ircfg_from_asmcfg(asmcfg)\n",
    "for lbl, irblk in viewitems(ircfg.blocks):\n",
    "    print(irblk)"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {},
   "outputs": [],
   "source": [
    "# Preparing the initial symbols for regs and mems\n",
    "symbols_init =  {}\n",
    "\n",
    "# for regs\n",
    "for i, r in enumerate(all_regs_ids):\n",
    "    symbols_init[r] = all_regs_ids_init[i]\n",
    "\n",
    "# for mems\n",
    "# 0xdeadbeef is the mark to stop the exploring\n",
    "symbols_init[ExprMem(ExprId('ESP_init', 32), 32)] = ExprInt(0xdeadbeef, 32)\n",
    "\n",
    "final_states = []"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {},
   "outputs": [],
   "source": [
    "explore(ir_arch, \n",
    "        target_addr, \n",
    "        symbols_init, \n",
    "        ircfg, \n",
    "        lbl_stop=0xdeadbeef, \n",
    "        final_states=final_states)"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {},
   "outputs": [],
   "source": [
    "executed_lockey   = []\n",
    "unexecuted_lockey = []\n",
    "\n",
    "# The IR nodes which are included in one of paths were executed.\n",
    "for final_state in final_states:\n",
    "    if final_state.result:\n",
    "        for node in final_state.path_history:\n",
    "            if isinstance(node, int):\n",
    "                lbl = ircfg.get_loc_key(node)\n",
    "            elif isinstance(node, ExprInt):\n",
    "                lbl = ircfg.get_loc_key(node)\n",
    "            elif isinstance(node, LocKey):\n",
    "                lbl = node.loc_key\n",
    "\n",
    "            if lbl not in executed_lockey:\n",
    "                executed_lockey.append(lbl)\n",
    "                \n",
    "# Otherwise, the IR nodes which are not included in any path were not executed.\n",
    "for lbl, irblock in viewitems(ircfg.blocks):\n",
    "    if lbl not in executed_lockey:\n",
    "        unexecuted_lockey.append(lbl)"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {},
   "outputs": [],
   "source": [
    "print(executed_lockey)\n",
    "print(unexecuted_lockey)\n",
    "print('len(executed_lockey):', len(executed_lockey))\n",
    "print('len(unexecuted_lockey):', len(unexecuted_lockey))"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {},
   "outputs": [],
   "source": [
    "# Generate an IDC script to set color on un-executed basic blocks.\n",
    "if idc:\n",
    "    to_idc(unexecuted_lockey, asmcfg)"
   ]
  }
 ],
 "metadata": {
  "kernelspec": {
   "display_name": "Python 3",
   "language": "python",
   "name": "python3"
  },
  "language_info": {
   "codemirror_mode": {
    "name": "ipython",
    "version": 3
   },
   "file_extension": ".py",
   "mimetype": "text/x-python",
   "name": "python",
   "nbconvert_exporter": "python",
   "pygments_lexer": "ipython3",
   "version": "3.6.9"
  }
 },
 "nbformat": 4,
 "nbformat_minor": 4
}
